(begin-proof )
(establish_and_6 obj1 max)
(establish_or_7_1 obj1 max)
(establish_exists_8 obj1 max)
(establish_and_6 max zero)
(establish_or_7_1 max zero)
(establish_exists_8 max zero)
(establish_and_6 zero obj1)
(establish_or_7_1 zero obj1)
(establish_exists_8 zero obj1)
(establish_forall_9_base )
(establish_forall_9_inductive zero obj1)
(establish_forall_9_inductive obj1 max)
(prove-goal )
